Issue2828.agda:12,9-11
⊤ !=< X of type Set
when checking that the expression tt has type X
